<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Simple</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Background">\title{simple}

\p{This is test file}
</a><a id="39" class="Markup">\agda{</a>
<a id="46" class="Keyword">module</a> <a id="53" href="Simple.html" class="Module">Simple</a> <a id="60" class="Keyword">where</a>

  <a id="69" class="Keyword">data</a> <a id="Bool"></a><a id="74" href="Simple.html#74" class="Datatype">Bool</a> <a id="79" class="Symbol">:</a> <a id="81" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="85" class="Keyword">where</a>
            <a id="Bool.true"></a><a id="103" href="Simple.html#103" class="InductiveConstructor">true</a> <a id="108" class="Symbol">:</a> <a id="110" href="Simple.html#74" class="Datatype">Bool</a>
            <a id="Bool.false"></a><a id="127" href="Simple.html#127" class="InductiveConstructor">false</a> <a id="133" class="Symbol">:</a> <a id="135" href="Simple.html#74" class="Datatype">Bool</a>

  <a id="a"></a><a id="143" href="Simple.html#143" class="Function">a</a> <a id="145" class="Symbol">:</a> <a id="147" href="Simple.html#74" class="Datatype">Bool</a>
  <a id="154" href="Simple.html#143" class="Function">a</a> <a id="156" class="Symbol">=</a> <a id="158" href="Simple.html#103" class="InductiveConstructor">true</a>
<a id="163" class="Markup">}</a><a id="164" class="Background">
</a></pre></body></html>